$\forall$$r$:CRng, $p$:Ideal($r$)\{i\}, $d$:detach\_fun($\mid$$r$$\mid$;$p$).
\\[0ex]($\forall$$u$:$\mid$$r$$\mid$. SqStable($p$($u$))) $\Rightarrow$ (IsPrimeIdeal($r$;$p$) $\Leftarrow\!\Rightarrow$ IsIntegDom($r$ / $d$))